FDL - Nuprl Lemma : es-increasing-sequence2

Nuprl Lemma : es-increasing-sequence2

es:ES, m:

, f:(

m

E). (

i:

(m-1). (f(i) <loc f(i+1)))

(

i:

m, j:

(i+1). f(j)

f(i) )

Definitions {i..j}, t T, x:A. B(x), P Q, Dec(P), P Q, ES, , E, AB, P & Q, i j < k, False, A, (e <loc e'), Prop, e e' , {T}, SQType(T)

Lemmas es-le-self, subtype rel self, es-locl wf, le wf, int seg wf, es-E wf, nat plus wf, event system wf, es-increasing-sequence, decidable int equal